Inference at * 2 0 
Iof proof for Lemma exists functionality wrt iff:



1. S : Type
2. T : Type
3. P : S
4. Q : S
5. S = T
6. x:S. P(x)  Q(x)
7. y:T. Q(y)
  x:S. P(x) 

latex

 by PERMUTE{1:n, 1:n, 2:n} 

latex

 1: .....wf..... NILNIL

 1: 7. y : T
 1: 8. Q(y)
 1:   y  S
 2: .....wf..... NILNIL

 2: 7. y : T
 2: 8. Q(y)
 2: 9. x : S
 2:   P(x)  
 .

Definitions

f(a), t  T, x:A  B(x), x(s), s = t, , x:AB(x), Type, P  Q, P  Q, P & Q, P  Q, x:A. B(x), x:A. B(x)